Inference at * 1 
Iof proof for Lemma p-conditional-domain:



1. A : Type
2. B : Type
3. f : A(B + Top)
4. g : A(B + Top)
5. x : A
6. isl(if isl(f(x)) then f(x) else g(x) fi )
7. (isl(f(x)))
  isl(g(x)) 

latex

 by ((SplitOnHypITE (-2)) 
CollapseTHEN (Auto)) 

latex

Co.

Definitions	P  Q, left + right, s ~ t, SQType(T), {T}, P  Q, P & Q, x:A  B(x), x:AB(x), P  Q, False, , s = t, , b, t  T, A, b, x:A. B(x)
Lemmas	bool cases, eqtt to assert, bool sq, iff transitivity, eqff to assert, assert of bnot, bool wf, assert wf, bnot wf, not wf